00100	GIVEAX(LISP1,ISSET SEXP);
00200	
00300	GIVEAX(LISP2,(∀ X)(∀ Y)(XεSEXP ∧ YεSEXP ⊃ CONS(X,Y)εSEXP
00400		∧ ¬ATOM CONS(X,Y) ∧ CAR CONS(X,Y) = X ∧
00500		CDR CONS(X,Y) = Y));
00600	
00700	GIVEAX(LISP3,(∀ X)(XεSEXP ∧ ¬ATOM SEXP ⊃ CAR X ε SEXP
00800		∧ CDR X ε SEXP ∧ X = CONS(CAR X,CDR X));
00900	
01000	GIVEAX(LISP4,(∀ U)(ISSET U ∧ U⊂SEXP ∧ (∀ X)(XεSEXP ∧
01100		ATOM X ⊃ XεU) ∧ (∀ X)(XεSEXP ∧ CAR X ε U
01200		∧ CDR X ε U ⊃ XεU) ⊃ U=SEXP));
01300	
01400	GIVEAX(LISP5,¬(UUεSEXP));
01500	
01600	GIVEAX(LISP6,(∀ X)(XεSEXPE ≡ X=UU ∨ XεSEXP));
01700	
01800	GIVEAX(LISP7,SCORDERING LISPORD);
01900	
02000	GIVEAX(LISP8,DOMAIN LISPORD = SEXPE);
02050	
02100	GIVEAX(LISP9,TRIVIAL(LISPORD,SEXP));
     

02100	END;